== FairFifo
== & ((
i, x:Id. vartype(i;x) 
r M(i).ds(x))
== & (c
(i:Id, a:Action(i). (
(
isnull(a))) 
(valtype(i;a) r M(i).da(kind(a))))
== & (c
(l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(l,tg)))
== & (c
(i, x:Id. M(i).init(x,s(i;0).x))
== & (c
(i:Id, t:
.
== & (c
((isnull(a(i;t))))
== & (c
(((islocal(kind(a(i;t))))
== & (c
(( (M(i).pre(act(kind(a(i;t))),read-state(
x.s(i;t).x))
== & (c
(( & ma-random(M(i);
== & (c
(( & ma-random(valtype(i;a(i;t));
== & (c
(( & ma-random(val(a(i;t));i;act(kind(a(i;t)));w-knum(w;i;kind(a(i;t));t))))
== & (c
& (x:Id.
== & (c
& (M(i).ef(kind(a(i;t)),x,read-state(x.s(i;t).x),val(a(i;t)),q.s(i;t+1).x(q - 1)))
== & (c
& (l:IdLnk.
== & (c
& (M(i).send(kind(a(i;t));l;read-state(x.s(i;t).x);val(a(i;t));withlnk(l;m(i;t));i))
== & (c
& (x:Id.
== & (c
& ((M(i).frame(kind(a(i;t)) affects x)) (r:
. s(i;t).x(r + 1) = s(i;t+1).x(r)))
== & (c
& (l:IdLnk, tg:Id.
== & (c
& ((M(i).sframe(kind(a(i;t)) sends <l,tg>)) (w-tagged(tg;onlnk(l;m(i;t))) = []))))
== & (c
((i, a:Id, t:.
== & (c
((
t':
== & (c
((((t 
t')
== & (c
((& ((((isnull(a(i;t')))) c (kind(a(i;t')) = locl(a)))
== & (c
((& (
(a declared in M(i))
== & (c
((& ( unsolvable M(i).pre(a,read-state(x.s(i;t').x)))))
== & (c
& (i:Id, t:.
== & (c
& (((isnull(a(i;t))))
== & (c
& ( (x:Id.
== & (c
& ( (M(i).aframe(kind(a(i;t)) affects x)) (r:. s(i;t).x(r + 1) = s(i;t+1).x(r))))
== & (c
& (i, x:Id, k:Knd. (M(i).rframe(k reads x)) w-machine-independent(w;i;k;x))
== & (c
& (i:Id, t:.
== & (c
& (((isnull(a(i;t))))
== & (c
& ( (l:IdLnk.
== & (c
& ( (M(i).bframe(kind(a(i;t)) sends on l)) (onlnk(l;m(i;t)) = [])))))
clarification:
possible-world{i:l}
possible-world(D; w)
== fair-fifo{i:l}
== fair-fifo(w)
== & ((
i:Id, x:Id. w-vartype(w; i; x) r d-m(D; i).ds(x))
== & (c
(i:Id, a:w-action(w; i).
== & (c
((w-isnull(w; a))) (w-valtype(w; i; a) r d-m(D; i).da(w-kind(w; a))))
== & (c
(l:IdLnk, tg:Id. (w.M(l,tg)) r d-m(D; source(l)).da(rcv(l,tg)))
== & (c
(i:Id, x:Id. d-m(D; i).init(x,w-s(w; i; 0; x)))
== & (c
(i:Id, t:.
== & (c
((w-isnull(w; w-a(w; i; t))))
== & (c
(((islocal(w-kind(w; w-a(w; i; t))))
== & (c
(( (d-m(D; i).pre(act(w-kind(w; w-a(w; i; t))),read-state(x.w-s(w; i; t; x)))
== & (c
(( & ma-random(d-m(D; i);
== & (c
(( & ma-random(w-valtype(w; i; w-a(w; i; t));
== & (c
(( & ma-random(w-val(w; w-a(w; i; t));
== & (c
(( & ma-random(i;act(w-kind(w; w-a(w; i; t)));w-knum(w;i;w-kind(w; w-a(w; i; t));t))))
== & (c
& (x:Id.
== & (c
& (d-m(D; i).ef(w-kind(w; w-a(w; i; t)),
== & (c
& (x,
== & (c
& (read-state(x.w-s(w; i; t; x)),w-val(w; w-a(w; i; t)),q.w-s(w; i; (t+1); x)(q - 1)))
== & (c
& (l:IdLnk.
== & (c
& (d-m(D; i).send(w-kind(w; w-a(w; i; t));
== & (c
& (l;read-state(x.w-s(w; i; t; x));w-val(w; w-a(w; i; t));withlnk(l;w-m(w; i; t));i))
== & (c
& (x:Id.
== & (c
& ((d-m(D; i).frame(w-kind(w; w-a(w; i; t)) affects x))
== & (c
& ( (r:. w-s(w; i; t; x)(r + 1) = w-s(w; i; (t+1); x)(r) 
w-vartype(w; i; x)))
== & (c
& (l:IdLnk, tg:Id.
== & (c
& ((d-m(D; i).sframe(w-kind(w; w-a(w; i; t)) sends <l,tg>))
== & (c
& ( (w-tagged(tg;onlnk(l;w-m(w; i; t))) = [] (w-Msg(w) List)))))
== & (c
((i:Id, a:Id, t:.
== & (c
((t':
== & (c
((((t t')
== & (c
((& ((((w-isnull(w; w-a(w; i; t')))) c (w-kind(w; w-a(w; i; t')) = locl(a) Knd))
== & (c
((& ( (a declared in d-m(D; i))
== & (c
((& ( unsolvable d-m(D; i).pre(a,read-state(x.w-s(w; i; t'; x))))))
== & (c
& (i:Id, t:.
== & (c
& (((w-isnull(w; w-a(w; i; t))))
== & (c
& ( (x:Id.
== & (c
& ( (d-m(D; i).aframe(w-kind(w; w-a(w; i; t)) affects x))
== & (c
& ( (r:. w-s(w; i; t; x)(r + 1) = w-s(w; i; (t+1); x)(r) w-vartype(w; i; x))))
== & (c
& (i:Id, x:Id, k:Knd. (d-m(D; i).rframe(k reads x)) w-machine-independent(w;i;k;x))
== & (c
& (i:Id, t:.
== & (c
& (((w-isnull(w; w-a(w; i; t))))
== & (c
& ( (l:IdLnk.
== & (c
& ( (d-m(D; i).bframe(w-kind(w; w-a(w; i; t)) sends on l))
== & (c
& ( (onlnk(l;w-m(w; i; t)) = [] (w-Msg(w) List))))))